E,X1,X2:Type, info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), pred?:(E(?E)),
p:(e:E, l:IdLnk.
p:(e':E
p:((e'':E. 
p:((rcv?(e''))
p:( (sender(e'') = e)
p:( (link(e'') = l)
p:( (((e'' = e')  e'' < e')  (loc(e') = destination(l)  Id)))),
r:E.
SWellFounded(pred!(e;e'))
 (e:E. ((first(e)))  (loc(pred(e)) = loc(e)  Id))
 (e,e':E. (loc(e) = loc(e')  Id)  (pred?(e) = pred?(e'))  (e = e'))
 (rcv?(r))
 (r 
 rel_star(E; (x,y. ((first(y))) c (x = pred(y)  E))
 rel_star() sends-bound(p; sender(r); link(r))) 

latex

Definitions	ecase1(e;info;i.f(i);l,e'.g(l;e')), True, sends-bound(p; e; l), rel_plus(T; R), A c B, sender(e), link(e), first(e), pred(e), SWellFounded(R(x;y)), x,y. t(x;y), pred!(e;e'), x:A. B(x), b, rcv?(e), e < e', prop{i:l}, loc(e), destination(l), Unit, Id, IdLnk, guard(T), t  T, P  Q, x:A. B(x), A, False, P  Q, x f y, rel_star(T; R), P  Q
Lemmas	link wf, sender wf, sends-bound-property, IdLnk wf, Id wf, unit wf, ldst wf, loc wf, cless wf, rcv? wf, assert wf, pred! wf, strongwellfounded wf, pred wf, first wf, not wf, rel star weakening, cless-eq-loc, sends-bound wf, rel-plus-rel-star, true wf, false wf